$\forall$$A$:MsgA, $x$, $z$:Id, $k$:Knd, $s_{1}$, $s_{2}$:$A$.state, $v$:$A$.da($k$).
\\[0ex]ma{-}frame{-}compat($A$;$A$)
\\[0ex]$\Rightarrow$ $\neg$$A$.rframe($k$ reads $x$)
\\[0ex]$\Rightarrow$ ($s_{1}$ $\equiv$ $s_{2}$ mod $x$)
\\[0ex]$\Rightarrow$ $\neg$$z$ $=$ $x$
\\[0ex]$\Rightarrow$ $A$.ef($k$,$z$,$s_{1}$,$v$)?$s_{1}$($z$) $=$ $A$.ef($k$,$z$,$s_{2}$,$v$)?$s_{2}$($z$) $\in$ $A$.ds($z$)